COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	shankar[f86,jmc]		Shankar short form
C00005 ENDMK
C⊗;
shankar[f86,jmc]		Shankar short form

I. Shankar is being hired to replace Dr. Jussi Ketonen in an NSF sponsored
project on interactive theorem proving.  Ketonen went into industry on
leave, and his leave has just expired.  Shankar will lead the project.
Ketonen developed the interactive theorem prover EKL.  Shankar will
develop his own ideas in this area which may involve extending EKL
but more likely will involve a new prover based on his experience
at the University of Texas in using the Boyer-Moore theorem prover
to prove the Church-Rosser theorem and the Godel incompleteness theorem.

II. A. A full seaarch was not appropriate for this position, because
unique capabilities are involved.  Shankar is probably the only new
PhD in the area in the country, and certainly no-one else has pushed
such difficult theorems through an interactive prover.

B. No other candidates were considered.

C. The NSF grant is rather narrow in its scope, because it was obtained
with Ketonen's qualifications and research plans in mind.  However,
its major objective - developing an interactive theorem prover suitable
for difficult mathematical theorems - is one that Shankar shares with
Ketonen.  I (John McCarthy) learned about Shankar from Professor
Robert Boyer of the University of Texas, and I have been following
his work for several years and have read his reports.  Shankar gave
seminars on this work at Stanford at more than one stage of the work.
See IIA for Shankar's unique qualifications.